Formally prove `log2`

[QGarchery]

I see 2 ways we can do it:

• prove that our method works for every de Bruijn sequence. This is an elegant approach that would require to include precomputeRows in the formal verification
• prove that our current implementation with the particular de Bruijn sequence is correct, and in particular the hash table returns the expected value. It may be easier to do

[MerlinEgalite]

I think you know what I would say but I guess it's up to you 😇

[MerlinEgalite]

@QGarchery I guess this is something that @makcandrov can do?

[QGarchery]

Let's keep this for later, it's not a pressing issue