Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement checked exponentiation. #9479

Merged
merged 1 commit into from
Aug 18, 2020
Merged

Implement checked exponentiation. #9479

merged 1 commit into from
Aug 18, 2020

Conversation

chriseth
Copy link
Contributor

@chriseth chriseth commented Jul 22, 2020

Fixes #9110.
Fixes #8853.

@chriseth
Copy link
Contributor Author

Would be nice to know the gas costs of this.

@chriseth
Copy link
Contributor Author

The inner loop itself takes about 144 gas per iteration. For an exp that uses the full 8 iterations this is about 1200 gas per exp operation.

@chriseth
Copy link
Contributor Author

In comparison, the opcode itself costs 10 gas.

@hrkrshnn
Copy link
Member

hrkrshnn commented Jul 24, 2020

If the LHS of the operation is a Literal, can we write a version where the compiler computes the max-value of the exponent: 256/log_2(integer_literal) The code reverts during runtime if the exponent is greater than or equal to this value. Otherwise, we make a call to exp (or shl if base is 2)

I tried to look at all the non-trivial examples (i.e., not literal**literal) of exponentiation. All such cases had a literal as a base, mostly 2, some 10, one 256. Here is a list of use cases https://gist.github.com/hrkrshnn/c73874b150d4a2c1ec6ebbc345efa9b3

Copy link
Member

@leonardoalt leonardoalt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think @hrkrshnn 's idea should be implemented.
@chriseth what do you think?

@@ -0,0 +1,11 @@
contract C {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wasn't this test added in some other PR? Also, why not also via Yul?

{
solUnimplementedAssert(!_type.isSigned(), "");
solAssert(!_exponentType.isSigned(), "");
string functionName = "checked_exp_" + _type.identifier();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does _exponentType need to be in the function name identifier as well?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch!

solAssert(!dynamic_cast<IntegerType const&>(_exponentType).isSigned(), "");

m_context << Instruction::EXP;

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Extra blank

@chriseth
Copy link
Contributor Author

@hrkrshnn @leonardoalt you are right, we should certainly specialize this for literals. it might even make sense to add some conditional to check for the values of non-literals.

@chriseth
Copy link
Contributor Author

After the "optimization for small bases" commit, most of the tests will now not test the loop anymore...

@chriseth
Copy link
Contributor Author

@leonardoalt can we prove this code correct?

@chriseth
Copy link
Contributor Author

All of the examples in @hrkrshnn 's list, the bases were either 2, 10 or 256, so I added optimized version for those bases.

@leonardoalt
Copy link
Member

@leonardoalt can we prove this code correct?

with a few adjustments I think so

// b**e < 2**256 <=> e * log(b) < 256 * log(2) <=> e < 256 * log(2) / log(b)
if or(
and(lt(base, 11), lt(exponent, 78)),
and(lt(base, 257), lt(exponent, 33)),
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
and(lt(base, 257), lt(exponent, 33)),
and(lt(base, 257), lt(exponent, 32)),

Because 256**32 = 2**256 = UINT256_MAX + 1

// small base optimizations
if eq(base, 2) {
if gt(exponent, 255) { revert(0, 0) }
power := exp(2, exponent)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This will be converted to shl by the optimizer right?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can check, but manly, shl does not exist on all platforms.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually it seems we do not have such a rule. I will add it separately.

@chriseth
Copy link
Contributor Author

I just realized that functions containing leave cannot be inlined, which is of course fatal in case the exp function is used together with constants. That is another point in favour of replacing functions with constant arguments by copies. I will rewrite this without leave.

base := <cleanupFunction>(base)
exponent := <exponentCleanupFunction>(exponent)

// avoiding `leave` to allow this function to be inlined
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't the function too lengthy to be inlined?

@axic
Copy link
Member

axic commented Aug 5, 2020

Why do we need checked exponentiation for the yul IR, but not for the old codegen?

@ethereum ethereum deleted a comment from stackenbotten Aug 5, 2020
@ethereum ethereum deleted a comment from stackenbotten Aug 5, 2020
@ethereum ethereum deleted a comment from stackenbotten Aug 5, 2020
@ethereum ethereum deleted a comment from stackenbotten Aug 5, 2020
@ethereum ethereum deleted a comment from stackenbotten Aug 5, 2020
@chriseth
Copy link
Contributor Author

chriseth commented Aug 6, 2020

This function is tricky. We do not necessarily want it to be inlined, but we want information about the size of the base to be taken into account in the function. Currently, the optimizer can only do this through inlining. Using leave prevents it from being inlined because the concept cannot be adequately replaced in all cases.

In the end of course, we should write the code such that it is best readable and improve the optimizer instead, because Solidity code will also very likely use return.

If a function does not contain a leave inside a loop, we can pack it into for {} 1{} { ... break } and replace the leave by a break, but I am not sure how well the other parts of the optimizer will cope with that.

@chriseth
Copy link
Contributor Author

chriseth commented Aug 6, 2020

Reverted to the version that uses leave. Since most of the code is the same regardless of the type, we might consider extracting the part that does not depend on the type into its own function (which then takes max as an explicit parameter), which would reduce code duplication

@ethereum ethereum deleted a comment from stackenbotten Aug 6, 2020
// 0**0 == 1
switch exponent
case 0 { power := 1 leave }
case 1 { power := base leave }
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ouch, Yul looks weird with these statements on the same line :)

if and(exponent, 1)
{
// no check needed for positive power, because base >= power
if and(slt(power, 0), slt(power, sdiv(min, base))) { revert(0, 0) }
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was not able to find a test that does not revert if I comment out this line - maybe the check about base above is sufficient. Maybe someone can prove this superfluous.

Copy link
Member

@hrkrshnn hrkrshnn Aug 18, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's redundant because

  • max < |min|
  • |power| < |base| everywhere in the loop (except base = +1 or -1)
  • at this point, |base * base| <= max.
  • therefore |power * base| < |base * base| <= max < |min|. So there is no underflow.

@chriseth
Copy link
Contributor Author

I'm now confident this is a version that can be merged, so please review!

The version that optimizes constants and small values will be done in another PR.

Comment on lines 625 to 626
("maxValue", toCompactHexWithPrefix(u256(_type.maxValue())))
("minValue", toCompactHexWithPrefix(u256(_type.minValue())))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
("maxValue", toCompactHexWithPrefix(u256(_type.maxValue())))
("minValue", toCompactHexWithPrefix(u256(_type.minValue())))
("maxValue", toCompactHexWithPrefix(_type.max()))
("minValue", toCompactHexWithPrefix(_type.min()))

if and(exponent, 1)
{
// no check needed for positive power, because base >= power
if and(slt(power, 0), slt(power, sdiv(min, base))) { revert(0, 0) }
Copy link
Member

@hrkrshnn hrkrshnn Aug 18, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's redundant because

  • max < |min|
  • |power| < |base| everywhere in the loop (except base = +1 or -1)
  • at this point, |base * base| <= max.
  • therefore |power * base| < |base * base| <= max < |min|. So there is no underflow.

// f(int256,uint256): -2, 1 -> -2
// f(int256,uint256): -2, 2 -> 4
// f(int256,uint256): -7, 63 -> -174251498233690814305510551794710260107945042018748343
// f(int256,uint256): -128, 2 -> 0x4000
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add this:
// g(int256,uint256): -1, 115792089237316195423570985008687907853269984665640564039457584007913129639935 -> -1

A test case that loops 255 times.

// overflow check for base * base
if gt(base, div(max, base)) { revert(0, 0) }
if and(exponent, 1)
{
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@hrkrshnn simplified your proof a little - can you check, please?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@chriseth chriseth merged commit 17edf4f into develop Aug 18, 2020
@chriseth chriseth deleted the exp branch August 18, 2020 11:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[Sol->Yul] Support exponentiation in constants Compile the "eth2-deposit-contract" with the IR
5 participants