Clarity on uint overflow

[paulhauner]

We (Lighthouse) are interested in building a "panic-free" implementation of the state transitions. I think we're fairly close when compiled in Rust's "release" mode (optimized, production-ready), however for Rust's "debug" mode (slow but useful for troubleshooting) any integer overflow that is not explicitly handled causes a panic.

When it comes to these overflows we have two choices:

• Indicate that wrapping on overflow is desired behavior (viz., don't raise an exception).
• Return early with an error if an overflow is encountered (viz., raise an exception).

The specification uses uint... types that, as I understand it, have undefined behavior when it comes to overflow (perhaps this can be derived from the tests, but this doesn't feel authoritative enough to me). From "common sense", I would assume that uint64_max_value() + 1 == 0 and 0 - 1 == uint64_max_value(). I also note that a few comments that infer uint64 overflows:

Math safe up to ~10B ETH, afterwhich this overflows uint64.

Factored out from balance totals to avoid uint64 overflow

Factored out from penalty numerator to avoid uint64 overflow

So, I'm inferring that uint64 overflows, assuming that it's desired behavior and assuming the specifics of that behavior.

It would be nice to have some clarity around this behavior. I understand that there's an idea that "valid state transitions shouldn't lead to overflows", but when it comes to things like fuzzing it's nice to have a distinction between "expected wrapping overflow" and "unexpected wrapping overflow".

So in summary, I have a question and a request please:

• Question: is a state transition considered valid if integer arithmetic overflows?
• Request: Make the spec explicit about the behavior of overflows.

As always, thanks! :)

[JustinDrake]

So, I'm inferring that uint64 overflows, assuming that it's desired behavior and assuming the specifics of that behavior.

I'd say the desired outcome is that these overflows are (provably, e.g. using formal verification) not possible. If for some reason we (the spec designers) messed up then overflows should probably trigger an exception.

Question: is a state transition considered valid if integer arithmetic overflows?

I'd say "no", this is an invalid state transition.

Request: Make the spec explicit about the behavior of overflows.

Agreed. To the sentence "State transitions that trigger an unhandled exception (e.g. a failed assert or an out-of-range list access) are considered invalid." we could add "Integer overflows are also considered exceptions." Alternatively, I believe we can redefine the behaviour of Python's arithmetic operators (e.g. + and *) to trigger overflow exceptions.

[protolambda]

Alternatively, I believe we can redefine the behaviour of Python's arithmetic operators (e.g. + and *) to trigger overflow exceptions.

This is already implemented. However, it's difficult to catch the cases where it doesn't go through these checked coercions (a + b returns a python int, which is then coerced safely, checking bounds, back into the spec type). It's difficult because python is very different from rust here, where it accepts everything by default, and doesn't know unsigned integers natively.

Adding it to the spec as invalid-transition explicitly would be great 👍

[michaelsproul]

This is already implemented. However, it's difficult to catch the cases where it doesn't go through these checked coercions (a + b returns a python int, which is then coerced safely, checking bounds, back into the spec type). It's difficult because python is very different from rust here, where it accepts everything by default, and doesn't know unsigned integers natively.

I'm not a Python expert, but the uint types from remerkleable seems to work quite well for checked addition and subtraction. Multiplication of two uints returns an int however, which can exceed the bounds. Could we override __add__, __sub__ and __mul__ on the uint types for stronger guarantees? If they are all functions (uint, uint) -> uint that raise an exception on overflow, then that should be sufficient.

[MrChico]

It would be nice to have some clarity around this behavior. I understand that there's an idea that "valid state transitions shouldn't lead to overflows", but when it comes to things like fuzzing it's nice to have a distinction between "expected wrapping overflow" and "unexpected wrapping overflow".

While doing overflow analysis in k for get_attestation_deltas, we defined max and min values for the variables involved, treating overflows happening for input values given within these bounds as "unexpected" and overflows happening for values outside of this range as "expected" (or maybe, more accurately "unspecified" or "irrelevant"). It might be valuable to make these sanity bounds explicit in the spec

[protolambda]

uint base class in remerkleable (the SSZ library backing spec currently) has:

    def __add__(self, other):
        return self.__class__(super().__add__(self.__class__.coerce_view(other)))

    def __sub__(self, other):
        return self.__class__(super().__sub__(self.__class__.coerce_view(other)))

Adding these in next release, missed them earlier (thanks @michaelsproul):

    def __mul__(self, other):
        return self.__class__(super().__mul__(self.__class__.coerce_view(other)))

    def __floordiv__(self, other):  # Better known as "//"
        return self.__class__(super().__floordiv__(self.__class__.coerce_view(other)))

The other value is converted to the same type (raising an exception if the byte length of the types does not match), then the regular python integer operation runs, and then the result is converted into the uint type of the self value (the constructor checks underflows/overflows).

Formal verification/review are still good to have though, these python checks only help during runtime.

[dapplion]

Spec declares that

State transitions that cause a uint64 overflow or underflow are also considered invalid.

consensus-specs/specs/phase0/beacon-chain.md

Line 1249 in 1e552f1

The post-state corresponding to a pre-state `state` and a signed block `signed_block` is defined as `state_transition(state, signed_block)`. State transitions that trigger an unhandled exception (e.g. a failed `assert` or an out-of-range list access) are considered invalid. State transitions that cause a `uint64` overflow or underflow are also considered invalid.