Formally prove log2

No description provided.

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

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

@QGarchery

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

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

Navigation Menu