Handle integer_squareroot bound case

[hwwhww]

Credits to the University of Manchester Bounded Model Checking (BMC) project team: Bruno Farias, Youcheng Sun, and Lucas C. Cordeiro for reporting this issue! 🙏 💯

This team is an Ethereum Foundation ESP "Bounded Model Checking for Verifying and Testing Ethereum Consensus Specifications (FY22-0751)" project grantee. They used ESBMC model checker to find this issue.

Also, thanks to Mate Soos and Justin Traglia (@jtraglia) for helping verify the issue! 🙌

tl;dr

It's a spec bug, but it's impossible to produce it in the current mainnet.

Description

integer_squareroot raises ValueError exception when n is maxint of uint64, i.e., 2**64 - 1.

However, we only use integer_squareroot in

1. integer_squareroot(total_balance)
2. integer_squareroot(SLOTS_PER_EPOCH)

With the current Ether total supply + EIP-1559, it's unlikely to hit the overflow bound in a very long time. (🦇🔊)

That said, it should be fixed to return the expected value.

How did I fix it

To make minimal changes in the spec, this fix returns the hardcoded edge case result. It's not pretty, but it's an easy patch. I believe there are better solutions, but I'm inclined not to change the existing code much.

Given that 2**64 should be overflow when computing total balance, I think we are not able to provide clean "state transition" test vectors for it. Perhaps we can have another new "math" category test vectors later.

p.s. I talked to all the CL client teams about it before opening this PR. :)

[jtraglia]

It's nit-picky, but I think this would be better as UINT64_MAX. Where the second _ is removed and MAX is moved to the end. This aligns more with how other libraries do things:

• https://cplusplus.com/reference/climits/
• https://doc.rust-lang.org/std/u64/constant.MAX.html

Suggested change

	| `MAX_UINT_64` | `uint64(2**64 - 1)` |
	| `UINT64_MAX` | `uint64(2**64 - 1)` |

[etan-status]

Isn't this similar to increase_balance not checking for overflow, but if there is an EVM chain with a different total supply, and then the entire supply were to be deposited into a validator, and then they attest, that everything gets deleted?

As in, should increase_balance also be fixed to support different scales than what is being used on Ethereum Mainnet?

[hwwhww]

@etan-status

Right, so in specs, we generally said that the SSZ typing ValueError is considered invalid.

However, for this helper, it's interesting that clients implemented it in various ways! 😄 If clients use the optimized library to implement it, it won't overflow as pyspec did.

For this case, it's better to make integer_squareroot return the correct value when the input value n is in the valid domain. It protects any possible future use case when we may somehow call integer_squareroot(2**64 - 1) in spec writing.

[ralexstokes]

seems like a good fix!