Implement assert()

[axic]

Implement #1130.

[axic]

I think this shouldn't be a breaking change given we allow user methods to shadow globals. (Even with the other PR it will only be a warning.)

[chriseth]

You can actually use false here.

[chriseth]

There is a section in the documentation that lists all reasons for exceptions, please add assert also there.

[axic]

@chriseth Updated both.

[chriseth]

This is a bit too sloppy (people might stop reading here). What about:

Add ``assert(condition)``, which throws if condition is false.

[axic]

I can change these late today. Can you approve it? Would like to merge it before the weekend.

[chriseth]

if condition is false?

[wuestholz]

@axic @chriseth Could you please provide some more information about why you decided to treat assert-statements similar to throw-statements by encoding them using revert instructions?

Based on an earlier discussion (#1598) it would seem more natural to me to treat assertions like runtime errors (e.g., division by zero) by encoding them using invalid instructions.

Just to provide some background, I'm working on a formal analysis tool for EVM bytecode and it would be very useful if errors (i.e., implicit or explicit assertion violations) could be distinguished from parameter validation (i.e., explicit throws or assumption/precondition violations in the verification community).

[chriseth]

@wuestholz thanks for your input and for closely following the progress here! I indeed spent some thoughts on this but it seems not enough :-)

So the idea would be that safety conditions are violated if and only if INVALID can be reached in any way. External failures (failed call) and invalid input (manual throw) would not be considered violations of the safety conditions. I wonder whether conditions for invalid inputs can also be handled more expressively than if (x) revert();.

[chriseth]

Please see #1702

[axic]

assert() can be pretty much used for input validation, e.g. it falls into the same category as throw. Additionally, we plan to have the assert reason text supported, which is only possible with using REVERT.

[wuestholz]

@axic @chriseth Thank you very much for the quick reply! It seems like there are certain discrepancies here.

I believe my view is consistent with what @chriseth wrote above. All errors or violations of safety conditions would use INVALID, whereas throws would use REVERT.

@chriseth What exactly do you mean by failed calls? For instance, does this include calls that run out of gas?

Another way to express such input validation would be a precondition or an assume-statement: assume(expr). I think this would be somewhat nicer than throw statements (assume(false) is essentially throw), but this might be just due to my background. :) However, this wouldn't necessarily be backwards-compatible, if one would deprecate throw afterwards.

I understand the point about providing some indication of what went wrong (e.g., using a message). I think this would be nice for both errors and throws/reverts.

The cleanest solution might be to advocate an ASSERT opcode for the EVM that works similar to REVERT; i.e., take same inputs (incl. message), but possibly draining the gas like INVALID. What do you think? Would that be an option?

[axic]

My motivation was to use assert as means of input validation (I'd be lazy adding a if (x) revert(y) for every field).

Then again we could think about having:

• assume() (invalid) and assert() (revert)
• assert() (invalid) and ensure() (revert)

I don't see the possibility to introducing an ASSERT opcode anytime soon.

would deprecate throw afterwards.

Note, throw is kind of deprecated with the introduction of assert(). At least it was by the time it was merged.

[chriseth]

assume / assert sounds good. @axic your comment about not being able to specify a message only concerns messages where callers might react to automatically. If you want to provide a message to the user, you can do that also with an invalid opcode: PUSH "message" INVALID - it will be visible in the debugger. A caller might respond differently to a failed input assumption (this might be invalid internal state because some other transaction went in earlier, invalid input that can be reported back to the user or an interface that is not supported to be used in a certain way), but a failed internal assertions - there is nothing you can do and they should all be treated identically.

[wuestholz]

@chriseth @axic Great that PUSH allows for a convenient way to provide a message to the user in case of an assertion violation! (This would also be quite nice for "built-in" exceptions, such as division-by-zero.)

If deprecating throw is indeed an option I would go with the assume-assert solution I sketched earlier and allow for both commands to optionally take a message. Otherwise, a less invasive solution would keep throw and just change the encoding of assert as implemented in #1702.