Binary search can overflow (very unlikely for this contract)

[3esmit]

In minime, the function balanceOfAt, or totalSupplyAt, uses a binary search to look for history of value in a certain block height.
The implementation uses a binary search calculation that could overflow when searching in very large data sets.

https://github.com/vacp2p/minime/blob/1f6820c2450553a4c9a600a51c727619e68f0c02/contracts/MiniMeBase.sol#L424C28-L424C42

However, this is unlikely due the size of uint256, and we dont report bugs for when the size of this arrays gets filled up.

Anyway, I think this should be fixed because the code for binary search for sake of correctness, as any smart contract, no bugs should be allowed, and also this could be copied to use in another contract where this might not be the case.

Currently this is the implementation:
uint256 mid = (high + low + 1) / 2;

The correct way should be:
uint256 mid = low + ((high - low + 1) / 2);

[0x-r4bbit]

Interesting.
I wonder if this is something the certora prover could find, given a proper spec

[0x-r4bbit]

Unassigning as w're not working on this atm.