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

[leonardoalt]

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]

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

[leonardoalt]

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]

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]

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]

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]

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]

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]

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 :)