Skip to content

Commit 3cba99a

Browse files
committed
Cheaper expWad and lnWad via symmetric rationals
1 parent c251232 commit 3cba99a

5 files changed

Lines changed: 891 additions & 11 deletions

File tree

docs/utils/fixedpointmathlib.md

Lines changed: 37 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -147,10 +147,7 @@ Equivalent to `(x * y) / WAD` rounded down.
147147
### rawMulWad(uint256,uint256)
148148

149149
```solidity
150-
function rawMulWad(uint256 x, uint256 y)
151-
internal
152-
pure
153-
returns (uint256 z)
150+
function rawMulWad(uint256 x, uint256 y) internal pure returns (uint256 z)
154151
```
155152

156153
Equivalent to `(x * y) / WAD` rounded down, but without overflow checks.
@@ -201,10 +198,7 @@ Equivalent to `(x * WAD) / y` rounded down.
201198
### rawDivWad(uint256,uint256)
202199

203200
```solidity
204-
function rawDivWad(uint256 x, uint256 y)
205-
internal
206-
pure
207-
returns (uint256 z)
201+
function rawDivWad(uint256 x, uint256 y) internal pure returns (uint256 z)
208202
```
209203

210204
Equivalent to `(x * WAD) / y` rounded down, but without overflow and divide by zero checks.
@@ -256,6 +250,22 @@ Returns `exp(x)`, denominated in `WAD`.
256250
Credit to Remco Bloemen under MIT license: https://2π.com/22/exp-ln
257251
Note: This function is an approximation. Monotonically increasing.
258252

253+
### expWadFast(int256)
254+
255+
```solidity
256+
function expWadFast(int256 x) internal pure returns (int256 r)
257+
```
258+
259+
Returns `exp(x)`, denominated in `WAD`. Cheaper than `expWad`.
260+
Let `E = exp(x / 1e18) * 1e18` denote the exact, infinite-precision result.
261+
Never overestimates: the result is greater than `E * (1 - 2.58e-22) - 1`
262+
and not more than `E`, so it is `floor(E)` or `floor(E) - 1` whenever
263+
`x <= 8265113944572514620` (results up to `~3885 * 1e18`).
264+
`expWadFast(0) = 1e18` exactly.
265+
Monotonically increasing, including across all `2**k` seams.
266+
The bounds are certified by exact-rational interval proofs, reproducible via
267+
https://github.com/ddallaire/wad-exponentials
268+
259269
### lnWad(int256)
260270

261271
```solidity
@@ -266,10 +276,26 @@ Returns `ln(x)`, denominated in `WAD`.
266276
Credit to Remco Bloemen under MIT license: https://2π.com/22/exp-ln
267277
Note: This function is an approximation. Monotonically increasing.
268278

279+
### lnWadFast(int256)
280+
281+
```solidity
282+
function lnWadFast(int256 x) internal pure returns (int256 r)
283+
```
284+
285+
Returns `ln(x)`, denominated in `WAD`. Cheaper than `lnWad`.
286+
Let `L = ln(x / 1e18) * 1e18` denote the exact, infinite-precision result.
287+
Never overestimates: always returns `floor(L)` or `floor(L) - 1`.
288+
`lnWadFast(1e18) = 0` exactly. Monotonically increasing.
289+
The bounds are certified by exact-rational interval proofs, reproducible via
290+
https://github.com/ddallaire/wad-exponentials
291+
269292
### lambertW0Wad(int256)
270293

271294
```solidity
272-
function lambertW0Wad(int256 x) internal pure returns (int256 w)
295+
function lambertW0Wad(int256 x)
296+
internal
297+
pure
298+
returns (int256 w)
273299
```
274300

275301
Returns `W_0(x)`, denominated in `WAD`.
@@ -759,7 +785,7 @@ function lerp(uint256 a, uint256 b, uint256 t, uint256 begin, uint256 end)
759785
Returns `a + (b - a) * (t - begin) / (end - begin)`,
760786
with `t` clamped between `begin` and `end` (inclusive).
761787
Agnostic to the order of (`a`, `b`) and (`end`, `begin`).
762-
If `begins == end`, returns `t <= begin ? a : b`.
788+
If `begin == end`, returns `t <= begin ? a : b`.
763789

764790
### lerp(int256,int256,int256,int256,int256)
765791

@@ -773,7 +799,7 @@ function lerp(int256 a, int256 b, int256 t, int256 begin, int256 end)
773799
Returns `a + (b - a) * (t - begin) / (end - begin)`.
774800
with `t` clamped between `begin` and `end` (inclusive).
775801
Agnostic to the order of (`a`, `b`) and (`end`, `begin`).
776-
If `begins == end`, returns `t <= begin ? a : b`.
802+
If `begin == end`, returns `t <= begin ? a : b`.
777803

778804
### isEven(uint256)
779805

src/utils/FixedPointMathLib.sol

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -271,6 +271,84 @@ library FixedPointMathLib {
271271
}
272272
}
273273

274+
/// @dev Returns `exp(x)`, denominated in `WAD`. Cheaper than `expWad`.
275+
/// Let `E = exp(x / 1e18) * 1e18` denote the exact, infinite-precision result.
276+
/// Never overestimates: the result is greater than `E * (1 - 2.58e-22) - 1`
277+
/// and not more than `E`, so it is `floor(E)` or `floor(E) - 1` whenever
278+
/// `x <= 8265113944572514620` (results up to `~3885 * 1e18`).
279+
/// `expWadFast(0) = 1e18` exactly.
280+
/// Monotonically increasing, including across all `2**k` seams.
281+
/// The bounds are certified by exact-rational interval proofs, reproducible via
282+
/// https://github.com/ddallaire/wad-exponentials
283+
function expWadFast(int256 x) internal pure returns (int256 r) {
284+
unchecked {
285+
// Accept `-41446531673892822313 < x < 135305999368893231589` with a
286+
// single unsigned comparison; sort out the two edges on the cold path.
287+
if (uint256(x) + 41446531673892822312 >= 176752531042786053901) {
288+
// When the true result is less than 1 wei we return zero.
289+
// This happens when `x <= (log(1e-18) * 1e18) ~ -4.15e19`.
290+
if (x <= -41446531673892822313) return r;
291+
292+
/// @solidity memory-safe-assembly
293+
assembly {
294+
// When the result is greater than `(2**255 - 1) / 1e18` we can not
295+
// represent it as an int. This happens when
296+
// `x >= floor(log((2**255 - 1) / 1e18) * 1e18) ≈ 135`.
297+
mstore(0x00, 0xa37bfec9) // `ExpOverflow()`.
298+
revert(0x1c, 0x04)
299+
}
300+
}
301+
302+
// Convert `x` from `10**18` fixed point to `2**96` fixed point.
303+
x = (x << 78) / 5 ** 18;
304+
305+
// Reduce to `x' in (-½ ln 2, ½ ln 2) * 2**96` with `exp(x) = 2**k * exp(x')`.
306+
// `6196328019 = round(2**128 / (ln 2 * 2**96))`; `k` is in the range `[-60, 195]`.
307+
int256 k = (x * 6196328019 + 2 ** 127) >> 128;
308+
x = x - k * 54916777467707473351141471128;
309+
310+
// `exp(x') = (E + x' * O) / (E - x' * O)`, a symmetric rational with
311+
// `E`, `O` polynomials in `x'^2`. `E` is monic: its last Horner stage
312+
// needs no `>> 96`, so with the constant term pre-shifted, `e` and `t`
313+
// are in `2**192` basis. The coefficients are jointly fitted so that the
314+
// certified relative error stays one-sided after the margin below, and
315+
// the error at the `+½ ln 2` edge is negative, which makes every seam
316+
// between adjacent `2**k` octaves step upward (monotonicity).
317+
int256 u = (x * x) >> 96;
318+
int256 e = (((u + 66584530426202717196765975783591) * u) >> 96)
319+
+ 5993331421273161380223160234961546;
320+
e = e * u + (52742053377336245150083666490725880 << 96);
321+
int256 o =
322+
((3328678398953600544402144014937 * u) >> 96) + 799080153247570479545590910204849;
323+
o = ((o * u) >> 96) + 26371026688668122575032340971836885;
324+
int256 t = x * o;
325+
326+
/// @solidity memory-safe-assembly
327+
assembly {
328+
// Div in assembly because solidity adds a zero check despite the unchecked.
329+
// The denominator is positive on the whole reduced domain.
330+
r := sdiv(add(e, t), sar(96, sub(e, t)))
331+
}
332+
333+
// Multiply by `2**k * 1e18 / 2**96`, less a margin that keeps the result
334+
// at or below `E` at every certified error extreme. `r < 1.5 * 2**96`,
335+
// so the product cannot overflow, and the shift amount is never negative.
336+
r = int256(
337+
(uint256(r) * 633825300114114700748270193445868131307960658286) >> uint256(195 - k)
338+
);
339+
340+
/// @solidity memory-safe-assembly
341+
assembly {
342+
// `exp(0) = 1` is the only exact integer result in the domain; the
343+
// margin lands it one unit low, so add one back exactly there.
344+
// The reduced `x` is zero iff the input was zero (the truncated
345+
// base conversion never lands on `k * 54916777467707473351141471128`
346+
// for any other input; checked exhaustively for every `k`).
347+
r := add(iszero(x), r)
348+
}
349+
}
350+
}
351+
274352
/// @dev Returns `ln(x)`, denominated in `WAD`.
275353
/// Credit to Remco Bloemen under MIT license: https://2π.com/22/exp-ln
276354
/// Note: This function is an approximation. Monotonically increasing.
@@ -346,6 +424,85 @@ library FixedPointMathLib {
346424
}
347425
}
348426

427+
/// @dev Returns `ln(x)`, denominated in `WAD`. Cheaper than `lnWad`.
428+
/// Let `L = ln(x / 1e18) * 1e18` denote the exact, infinite-precision result.
429+
/// Never overestimates: always returns `floor(L)` or `floor(L) - 1`.
430+
/// `lnWadFast(1e18) = 0` exactly. Monotonically increasing.
431+
/// The bounds are certified by exact-rational interval proofs, reproducible via
432+
/// https://github.com/ddallaire/wad-exponentials
433+
function lnWadFast(int256 x) internal pure returns (int256 r) {
434+
/// @solidity memory-safe-assembly
435+
assembly {
436+
// Compute `k = log2(x) - 96`, `r = 159 - k = 255 - log2(x) = 255 ^ log2(x)`.
437+
r := shl(7, lt(0xffffffffffffffffffffffffffffffff, x))
438+
r := or(r, shl(6, lt(0xffffffffffffffff, shr(r, x))))
439+
r := or(r, shl(5, lt(0xffffffff, shr(r, x))))
440+
r := or(r, shl(4, lt(0xffff, shr(r, x))))
441+
r := or(r, shl(3, lt(0xff, shr(r, x))))
442+
// We place the check here for more optimal stack operations.
443+
if iszero(sgt(x, 0)) {
444+
mstore(0x00, 0x1615e638) // `LnWadUndefined()`.
445+
revert(0x1c, 0x04)
446+
}
447+
// forgefmt: disable-next-item
448+
r := xor(r, byte(and(0x1f, shr(shr(r, x), 0x8421084210842108cc6318c6db6d54be)),
449+
0xf8f9f9faf9fdfafbf9fdfcfdfafbfcfef9fafdfafcfcfbfefafafcfbffffffff))
450+
451+
// Reduce range of x to (1, 2) * 2**96
452+
// ln(2^k * x) = k * ln(2) + ln(x)
453+
x := shr(159, shl(r, x))
454+
455+
// `s = (x - sqrt(2)) * 2**96 / (x + sqrt(2))`, so that
456+
// `ln(x) = ln(2)/2 + 2 * atanh(s)`. Centering on `sqrt(2)` halves the
457+
// fit domain: `|s| <= 3 - 2 * sqrt(2)`.
458+
let s :=
459+
sdiv(
460+
shl(96, sub(x, 112045541949572279837463876455)),
461+
add(x, 112045541949572279837463876455)
462+
)
463+
464+
// `2 * atanh(s) = s * A(w) / B(w)`, a (3, 3)-term odd rational in `w = s^2`.
465+
let w := sar(96, mul(s, s))
466+
let a :=
467+
add(
468+
sar(96, mul(sub(w, 1813347344949966953757847210329), w)),
469+
5824670411451500986303020460168
470+
)
471+
a := sub(sar(96, mul(a, w)), 4518264490991587979207438354337)
472+
let b :=
473+
sub(
474+
sar(96, mul(188151507788160136135094921663, w)),
475+
1676640319226537252003611223372
476+
)
477+
b := add(sar(96, mul(b, w)), 3665379287557676720634158507137)
478+
b := sub(sar(96, mul(b, w)), 2259132245495793985525851698055)
479+
480+
// `B` is bounded away from zero on the whole domain.
481+
let p := sdiv(mul(s, a), b)
482+
483+
// Add `(2k + 1) * ln(2)/2` and `ln(2**96 / 10**18)`, then convert to `WAD`,
484+
// all in `5**18 * 2**192` basis. The additive constant is lowered by a
485+
// certified margin (~0.0417 wei) so the accumulator never exceeds
486+
// `L * 2**174`; downward errors total under 1 wei, so `sar(174, p)`
487+
// lands on `floor(L)` or `floor(L) - 1`.
488+
p := mul(302231454903657293676544000000000000000000, p)
489+
p := add(
490+
mul(
491+
8298788776342807110743642979096973734596910279609939088954046749604186,
492+
sub(319, shl(1, r))
493+
),
494+
p
495+
)
496+
p := add(600920179829731861735705478226805774338444159116519230494951146088873754, p)
497+
r := sar(174, p)
498+
499+
// `ln(1e18 / 1e18) = 0` is the only exact integer result in the domain;
500+
// the margin lands it exactly on `-1`, so add one back precisely there.
501+
// (`floor(L) = -1` is unreachable: no input has `L in [-1, 0)`.)
502+
r := add(iszero(not(r)), r)
503+
}
504+
}
505+
349506
/// @dev Returns `W_0(x)`, denominated in `WAD`.
350507
/// See: https://en.wikipedia.org/wiki/Lambert_W_function
351508
/// a.k.a. Product log function. This is an approximation of the principal branch.

0 commit comments

Comments
 (0)