⚡️ Cheaper expWad and lnWad via symmetric rationals - #1546
Conversation
bb4aec7 to
46fcb70
Compare
|
@ddallaire Thanks for this PR! @duncancmt and I worked on the same thing ( I remember that at the time, we had an issue with the 18-decimal precision — we couldn’t get the true floor version of lnWad. @duncancmt then came up with a solution using ray precision. |
|
@atarpara I'll be waiting for comments 👍 Note that one CI test run is failing as the test outgrew the configured gas limit of 100M, please tell me if you want to bump the gas limit or no, I can always split the test contract on its own for |
|
My PR (and un-PR'd complementary work on Independent of the fixnum format, my implementation carefully quantifies the error in the approximation and compensates for/bounds it. Fundamentally, because @ddallaire , does your implementation have this rounding behavior? If not, that would be a nice improvement. I'm happy to work with you on that and try to formally verify that property using the same stack that I did with my implementation. [0] Although |
|
@duncancmt Thanks for the context on previous work. The goal of this implementation was to optimize the gas while being equally or more accurate than the previous version. If the current efforts are towards accuracy, you can disregard this PR. Error stats for these, feel free to validate:
The 6,6 version from my repo which also cuts down on gas reduces the error by a lot. |
|
Well, whether or not the stated error is adequate is a bit putting the cart before the horse. I think the major question is whether to keep the existing Independent of the answer to that question, I think it's very likely that your implementation could be coaxed into having floor-or-1-wei-less behavior with a bit of tweaking to the constants and a subtraction. My professional opinion is that having one-sided rounding error makes the design of systems with safe/conservative/optionality-adverse rounding behavior considerably easier, but this too could be a point for discussion. Certainly either implementation would be an improvement on the current one! 👍 |
|
I'm not going to chime in on the wad vs ray discussion as I have no horse in this. If the decision ends up going towards supporting both, I'd be happy to tweak both exp and ln function to make the error one sided as my PR doesn't supported that as is, my (6,6) exp implementation can be one-sided by removing a small bias, at the cost of 8 gas over the (5,5), unsure about the ln function as it's centered on |
|
@ddallaire I agree with the design direction suggested by @duncancmt , but I don't think Solady needs to move to Ray precision here. I'd prefer to keep the existing Wad/18-decimal basis and optimize around that. For Solady, the important property isn't higher internal precision, but rather that the approximation error is bounded and, more importantly, that the rounding direction is guaranteed. So I'd be happy with a solution that stays at Wad precision as long as we can guarantee that the result is always rounded in one direction (e.g. true floor for I think that property is more important for Solady than squeezing out additional precision, especially since it keeps the behavior predictable while keeping the implementation simple and efficient. And yes, I'd definitely like to formally verify that rounding-direction guarantee if possible. Maybe @duncancmt can help us with that. |
|
You can check my full implementation (again, at Ray-scale, but the general techniques may be applicable) in the branch in this PR 0xProject/0x-settler#599 . This is part of a larger PR stack, so I recommend pulling just the branch involved and examining the code/proof. I'm surprised that the 6-coeff version of |
|
Let’s support both. Just postfix the faster functions with “Fast”, while keeping the original functions in case some applications require the original precision. FixedPointMathLib is like a museum on the different numerical techniques.
In the comments, also give a link to the 0x-settler implementations in case viewers want to use the ray versions. |
46fcb70 to
3cba99a
Compare
Reverted every change from current functions, added the "fast" versions. Ensured that both functions are monotonically increasing, and that they both floor the result with the error bounded to at most 1 wei, while also preserving: Created a proof/test suite using z3 and everything I could think of, feel free to validate using Lean as I'm not familiar with that. I'll let @duncancmt reference his ray implementation in comments as I was unsure what the best links were for that. |
Gas Snapshot Comparison Report
|
|
Please reference: https://github.com/0xProject/0x-settler/blob/ea7f9721d3bc2cd7be849ec0ba46b0de3a403e1a/src/vendor/Exp.sol I owe you a code review on this PR, but I am a bit busy with the bills-paying work for the moment. My Lean proofs use largely the same techniques as your Z3 proofs. I think the TCB on my proofs is a bit smaller, but nothing immediately jumps out at my as "this proof is wrong". I'll review the proofs after I review the implementation after I get done with paying my bills 😅 |
4 participants
Description
Adds
expWadFastandlnWadFast: cheaper symmetric-rational implementations with acertified rounding direction.
expWadexpWadFastlnWadlnWadFastGuarantees (proved, not sampled):
lnWadFast(x)always returns⌊L⌋or⌊L⌋ − 1, whereL = ln(x/1e18) * 1e18is theexact result. It never overestimates.
lnWadFast(1e18) = 0exactly. Monotonicallyincreasing.
expWadFast(x)never overestimates the exactE = exp(x/1e18) * 1e18, and returns morethan
E·(1 − 2.58e-22) − 1. Forx ≤ 8265113944572514620(results up to ~3885e18) thatis
⌊E⌋or⌊E⌋ − 1; an absolute 1-wei bound for the full int256 codomain is notattainable in 256-bit arithmetic, so beyond that the bound is relative.
expWadFast(0) = 1e18exactly. Monotonically increasing, including across all 255 range-reduction seams.A full writeup and validation/proof toolkit is available here: https://github.com/ddallaire/wad-exponentials
Checklist
Ensure you completed all of the steps below before submitting your pull request:
forge fmt?forge test?