Integer overflow considerations

[paulhauner]

I'm considering integer overflows in Lighthouse and there are cases where I'm making some assumptions about what I think the spec means.

For example, consider this code in "verify attestations":

Verify that attestation.data.slot <= block.slot - MIN_ATTESTATION_INCLUSION_DELAY

As all of these variables are declared as uint64 it would be fair to assume that we're going to see potential under-flows in the first few blocks and the behavior of the function will be significantly different depending on whether or not the subtraction saturates or under-flows.

From my perspective it would be nice to see some explicitness around what to do in the case of overflows.

Or maybe all overflow scenarios have been considered and I'm missing some other checks that are normalizing behavior?

[JustinDrake]

In this particular instance it's an easy fix:

Verify that attestation.data.slot + MIN_ATTESTATION_INCLUSION_DELAY <= block.slot

I will go through the spec and fix what I find. The "harder" underflows are regarding balances and penalties. The spec has the following notice, admittedly not completely satisfactory:

Note: When applying penalties in the following balance recalculations implementers should make sure the uint64 does not underflow.

[paulhauner]

Thank you! :) I'll keep an eye out for your changes, then let you know if I notice any more.

[arnetheduck]

thanks @paulhauner! see also #160 - I found a few more of these but I'm also waiting for things to settle a bit given that there's lots of general bugfixing going on already :)

A similar "category" of underflows to look out for is close to genesis, where we do things like slot - EPOCH - slot at that time is 0 or small.

[JustinDrake]

So one idea is to have INITIAL_SLOT_NUMBER = 3 * EPOCH_LENGTH. Do you agree this solves the underflow problems with slots?

[arnetheduck]

I'm not familiar enough with the spec to say that this is sufficient to fully solve underflows, but gut-feeling-wise, it seems.. brittle.

Many of these issues happen in comparisons - another way to address those at least is to simply disallow subtraction and instead only allow addition. This solves the underflow problem, but not overflow problem.

#192 expresses a desire to be able to make formal claims about overflows as well - for example, one could make a formal claim about the system being both under- and overflow-free up to slot X.

[JustinDrake]

Paging in @djrtwo.

This solves the underflow problem, but not overflow problem.

What is the overflow problem? Can you point to an instance in the code?

[djrtwo]

When you flip a conditional that might have underflowed due to subtraction, you always get a conditional that might theoretically overflow due to addition.

That said, most of these issues had to do with subtracting small numbers from initial slots. If adding these small numbers to the slot causes an overflow, then we have more problems than that because we've exhausted our 64 bits worth of slots.

[arnetheduck]

Yup, agree it's theoretical at this stage - so it's more about understanding well what the bounds are, and thus being able to make good use of guarantees instead of hoping for the best :)

[paulhauner]

attestation.data.slot is "user supplied input" so we don't need our clocks to be trillions of years in the future to encounter the overflow introduced by swapping the underflow for an overflow . Someone just needs to craft a dodgy message.

Naive saturation has the effect that attestation.data.slot = 0 is always accepted when block.slot < MIN_ATTESTATION_INCLUSION_DELAY.

Assuming we don't want any attestations until the MIN_ATTESTATION_INCLUSION_DELAY'th block, my suggestion would be:

attestation.data.slot < max(0, block.slot - MIN_ATTESTATION_INCLUSION_DELAY - 1)

[arnetheduck]

Oops, I missed @paulhauner 's comment before doing #279.

[arnetheduck]

attestation.data.slot < max(0, block.slot - MIN_ATTESTATION_INCLUSION_DELAY - 1)

This still underflows, but good point about distinguishing "user data" from internal state, that presumably no longer is tainted.

The way forwards here might be to specify the semantics under no-overflow conditions / unbounded integers (still avoiding underflows), and address the issue in an appendix instead, that may or may not come with the spec.

[paulhauner]

attestation.data.slot < max(0, block.slot - MIN_ATTESTATION_INCLUSION_DELAY - 1)

This still underflows, but good point about distinguishing "user data" from internal state, that presumably no longer is tainted.

I assumed here that the spec uses Python for code examples and that block.slot is a Python int. This assumption is certainly questionable as the spec also declares block.slot to be a unit64.

This raises an interesting point that the spec uses an effectively undefined type for all uint<x> variants. Whilst we can make reasonable assumptions about how a Python 'uint64' behaves, AFAIK it is ultimately undefined. I'm not up to speed on this modern typed-Python stuff so maybe I'm missing something.

The way forwards here might be to specify the semantics under no-overflow conditions / unbounded integers (still avoiding underflows), and address the issue in an appendix instead, that may or may not come with the spec.

This could work. We could also define "saturating" methods that assume the Python the int type. This keeps within the bounds of well-defined Python. I take inspiration from Rust's u64::saturating_sub() style terminology here.

attestation.data.slot < saturating_sub(block.slot - (MIN_ATTESTATION_INCLUSION_DELAY - 1))

Assuming MIN_ATTESTATION_INCLUSION_DELAY > 0.

[arnetheduck]

python integers are essentially what are called unbounded bigints in statically typed languages - there's no concept of unsigned or bit length in python itself outside of its serialization/marshalling/interop modules - this is the translation friction we're encountering when trying to stuff what's in the spec into more limited types.

[arnetheduck]

While I have it in my head, I would jot down another common issue to watch out for with uint64: most JSON parsers use an IEEE754 double to represent anything that looks like a number, thus you get only 53 bits of precision, meaning that the lower bits are lost on large numbers (like justification_bitfield) -

Not a direct issue for compiled languages and controlled environments, but it shuts out a class of ready-made web-tools tools - this will be of interest for the testing effort which currently is looking at YAML - in some languages, a custom YAML/JSON parser will need to be used, or the numbers in question will have to be encoded as strings instead.

[JustinDrake]

Closing as I think underflows and overflows are now handled (e.g. with the GENESIS_SLOT chosen to be >> 0). Please reopen if we missed something!