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

Another attempt on SafeMath assert->require but for a different reason #1120

Closed
leonardoalt opened this Issue Jul 26, 2018 · 10 comments

Comments

Projects
None yet
4 participants
@leonardoalt
Contributor

leonardoalt commented Jul 26, 2018

The different reason is the formal verification module we're building in Solidity. I'll start with a general argument from my side, then I'll talk about the FV module.

I've read the multiple discussions in different issues/PRs, and first of all I need to say that I do disagree with having asserts in SafeMath. What the code does is filtering inputs, therefore requires should be used.
I've also read that the idea is that the users should filter their input, and SafeMath would use the assertions to enforce no overflow. Well, nobody does it, and the reason is that the asserts in SafeMath already do kind of the same, so why would people bother? Moreover, if users filter their inputs with require(b <= a), for example, then having an extra assert(b <= a) from SafeMath's sub is just a waste of gas.

Assuming that users do not filter their input and rely on SafeMath to guarantee no underflows/overflows, this breaks formal verification. The reason is that the verifier sees no filtering (no assumptions on the input), and then sees the assertion assert(b <= a) which it tries to prove, since it is a verification target. The verifier will report that the assertion is not true for all cases, and easily provide counterexamples, since there are no assumptions on a and b.

So, from a verification perspective it would also make more sense to have requires in SafeMath, such that the underflow/overflow cases would be simply filtered out of the execution path, and the rest of the path would have the safe invariant due to an assumption, not a target.

I'd love to hear your thoughts on it, even though it's a repetitive discussion...

@nventuro

This comment has been minimized.

Show comment
Hide comment
@nventuro

nventuro Jul 26, 2018

Member

Thanks for bringing this up @leonardoalt! Could you provide some examples on what you'd consider valid uses of assert?

Member

nventuro commented Jul 26, 2018

Thanks for bringing this up @leonardoalt! Could you provide some examples on what you'd consider valid uses of assert?

@sohkai sohkai referenced this issue Jul 26, 2018

Closed

feat: GentleSafeMath #1121

4 of 4 tasks complete

@shrugs shrugs referenced this issue Jul 27, 2018

Closed

Improved error handling style: assert -> require #778

4 of 4 tasks complete
@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Jul 27, 2018

Contributor

Hi @nventuro

One simple example could be:

function max(uint a, uint b) returns (uint) {
  uint c = a;
  if (b > c)
    c = b;
  assert(c >= a && c >= b);
  return c;
}

Of course this is a very simple example, but it illustrates that the invariant c >= a && c >= b should be true before the assert no matter what input values are given, the contract's state etc, therefore an assertion fail means a bug somewhere.

Another simple example:

function transfer(address to, uint amount) {
  require(balance[msg.sender] >= amount);
  uint sum = balance[msg.sender] + balance[to];
  balance[msg.sender] -= amount;
  balance[to] += amount;
  uint newSum = balance[msg.sender] + balance[to];
  assert(sum == newSum);
}

Similarly, the assertion should be true regardless the state of the whole thing.

Another more complex example would be, that after sorting an array, you could assert for each position that the element is <= the next.

Summary: conditions in asserts should be true no matter what before the assert.

So I think in the end it kinda comes down to what's expected from the user, and what should the user expect from SafeMath.
@shrugs I hope it's ok to copy over here what you said in #778:
"they should be invariants but obviously they aren't because nobody is doing requires before calling safemath anyway"
In my opinion:

  1. If the idea is that users should filter inputs and SafeMath only enforces it, then assert is correct;
  2. If the users don't have to guarantee the invariants and SafeMath is used as the input filter, then require is correct.

From a practical verification point of view: if 1 is the case, people have been doing it wrong which leads to me having to think about hacks in the verification tool to find those cases :p

Contributor

leonardoalt commented Jul 27, 2018

Hi @nventuro

One simple example could be:

function max(uint a, uint b) returns (uint) {
  uint c = a;
  if (b > c)
    c = b;
  assert(c >= a && c >= b);
  return c;
}

Of course this is a very simple example, but it illustrates that the invariant c >= a && c >= b should be true before the assert no matter what input values are given, the contract's state etc, therefore an assertion fail means a bug somewhere.

Another simple example:

function transfer(address to, uint amount) {
  require(balance[msg.sender] >= amount);
  uint sum = balance[msg.sender] + balance[to];
  balance[msg.sender] -= amount;
  balance[to] += amount;
  uint newSum = balance[msg.sender] + balance[to];
  assert(sum == newSum);
}

Similarly, the assertion should be true regardless the state of the whole thing.

Another more complex example would be, that after sorting an array, you could assert for each position that the element is <= the next.

Summary: conditions in asserts should be true no matter what before the assert.

So I think in the end it kinda comes down to what's expected from the user, and what should the user expect from SafeMath.
@shrugs I hope it's ok to copy over here what you said in #778:
"they should be invariants but obviously they aren't because nobody is doing requires before calling safemath anyway"
In my opinion:

  1. If the idea is that users should filter inputs and SafeMath only enforces it, then assert is correct;
  2. If the users don't have to guarantee the invariants and SafeMath is used as the input filter, then require is correct.

From a practical verification point of view: if 1 is the case, people have been doing it wrong which leads to me having to think about hacks in the verification tool to find those cases :p

@dddejan

This comment has been minimized.

Show comment
Hide comment
@dddejan

dddejan Jul 27, 2018

We're also playing with verification and moving the assert -> requires seems like the right thing to do (or at least if would be very helpful). Since the semantics are the same modulo gas, it's more about intent.

For verification purposes we treat

  • asserts as "find an execution that fails the assert, or show that none exists";
  • requires as "assume this holds while proving stuff that follows it".

The intent doe SafeMath is more in line with "let's assume that this holds" and use it (and if doesn't hold, it's OK due to revert). Considering the amount of contracts using SafeMath this is a big deal for verification attempts since, in most cases, it's not hard to trigger the overflows and these would then be reported as bugs (while they shouldn't).

dddejan commented Jul 27, 2018

We're also playing with verification and moving the assert -> requires seems like the right thing to do (or at least if would be very helpful). Since the semantics are the same modulo gas, it's more about intent.

For verification purposes we treat

  • asserts as "find an execution that fails the assert, or show that none exists";
  • requires as "assume this holds while proving stuff that follows it".

The intent doe SafeMath is more in line with "let's assume that this holds" and use it (and if doesn't hold, it's OK due to revert). Considering the amount of contracts using SafeMath this is a big deal for verification attempts since, in most cases, it's not hard to trigger the overflows and these would then be reported as bugs (while they shouldn't).

@nventuro

This comment has been minimized.

Show comment
Hide comment
@nventuro

nventuro Jul 28, 2018

Member

I see what you mean and agree with the raised points. Would asserts be optimized out in a production build, then?

Also, regarding SafeMath - this is the current implementation of div:

function div(uint256 a, uint256 b) internal pure returns (uint256) {
  // assert(b > 0); // Solidity automatically throws when dividing by 0
  // uint256 c = a / b;
  // assert(a == b * c + a % b); // There is no case in which this doesn't hold
  return a / b;
}

Would you suggest changing that first comment to require(b > 0), to prevent Solidity from throwing? (in line with @sohkai's PR, #1121).

Member

nventuro commented Jul 28, 2018

I see what you mean and agree with the raised points. Would asserts be optimized out in a production build, then?

Also, regarding SafeMath - this is the current implementation of div:

function div(uint256 a, uint256 b) internal pure returns (uint256) {
  // assert(b > 0); // Solidity automatically throws when dividing by 0
  // uint256 c = a / b;
  // assert(a == b * c + a % b); // There is no case in which this doesn't hold
  return a / b;
}

Would you suggest changing that first comment to require(b > 0), to prevent Solidity from throwing? (in line with @sohkai's PR, #1121).

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Jul 30, 2018

Contributor

asserts are still used as runtime checks that might catch compiler/EVM/etc bugs, so I wouldn't remove it even if a static analyzer says the assertion is true.

Regarding div: yes, I'd do the same as #1121. My personal reasoning is that if I'm writing a contract without SafeMath I'll explicitly add such a require. If I'm using SafeMath I'd expect it to keep the path clean for me everywhere.

Contributor

leonardoalt commented Jul 30, 2018

asserts are still used as runtime checks that might catch compiler/EVM/etc bugs, so I wouldn't remove it even if a static analyzer says the assertion is true.

Regarding div: yes, I'd do the same as #1121. My personal reasoning is that if I'm writing a contract without SafeMath I'll explicitly add such a require. If I'm using SafeMath I'd expect it to keep the path clean for me everywhere.

@nventuro nventuro referenced this issue Jul 30, 2018

Merged

Add Modulo operation for getting the quotient #915

4 of 4 tasks complete
@nventuro

This comment has been minimized.

Show comment
Hide comment
@nventuro

nventuro Jul 30, 2018

Member

I just found a curious situation in #915, where an assert was added in the manner you describe: coveralls is now reporting our test coverage dropped, since that assertion is always true (as expected). I looked into solidity-coverage a bit, and they consider this the intended behavior.

I worry other tools may be taking the same approach, leading to issues due to different interpretations on the semantics of assert. What do you think about this?

Member

nventuro commented Jul 30, 2018

I just found a curious situation in #915, where an assert was added in the manner you describe: coveralls is now reporting our test coverage dropped, since that assertion is always true (as expected). I looked into solidity-coverage a bit, and they consider this the intended behavior.

I worry other tools may be taking the same approach, leading to issues due to different interpretations on the semantics of assert. What do you think about this?

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Aug 1, 2018

Contributor

In my opinion they got asserts wrong. As you just said, it is expected that the assertion is always true, and if a test case breaks an assertion there should be a bug, therefore it shouldn't be considered in coverage.

I see your point about a consistent interpretation of asserts throughout the projects. I'm not aware of other projects interpreting asserts like that, even though they probably exist.
Ideally we'd need everyone on the same page, even if it takes some time.

Contributor

leonardoalt commented Aug 1, 2018

In my opinion they got asserts wrong. As you just said, it is expected that the assertion is always true, and if a test case breaks an assertion there should be a bug, therefore it shouldn't be considered in coverage.

I see your point about a consistent interpretation of asserts throughout the projects. I'm not aware of other projects interpreting asserts like that, even though they probably exist.
Ideally we'd need everyone on the same page, even if it takes some time.

@nventuro

This comment has been minimized.

Show comment
Hide comment
@nventuro

nventuro Aug 3, 2018

Member

I created an issue on their repo to get their opinions regarding this, and see if we can start getting the community on board with this proposal :)

Member

nventuro commented Aug 3, 2018

I created an issue on their repo to get their opinions regarding this, and see if we can start getting the community on board with this proposal :)

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Aug 3, 2018

Contributor

Nice, thanks @nventuro !

Contributor

leonardoalt commented Aug 3, 2018

Nice, thanks @nventuro !

@frangio

This comment has been minimized.

Show comment
Hide comment
@frangio

frangio Aug 7, 2018

Member

Thanks for such an interesting discussion guys! I was convinced that we should change SafeMath to use require.

Member

frangio commented Aug 7, 2018

Thanks for such an interesting discussion guys! I was convinced that we should change SafeMath to use require.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment