Adding a comment for explaining the last statement in the fls function

[PaulRBerg]

I was looking at the fls function in LibBit, and the last statement caught my attention:

solady/src/utils/LibBit.sol

Lines 35 to 37 in 5d0198b

	r := or(r, byte(shr(251, mul(x, shl(224, 0x07c4acdd))),
	0x0009010a0d15021d0b0e10121619031e080c141c0f111807131b17061a05041f))
	}

It would be helpful to provide an explainer comment above this line, so that readers of the contract know why you use 251, 224, and the other hardcoded values in this function.

[Vectorized]

Commenting for posterity.

fls uses magic numbers found via z3.

from z3 import *
import math

lookup = lambda x, l: (l >> ((31 - (x & 31)) << 3)) & 0xff

l = BitVec('l', 256)
q = BitVec('q', 256)

solve(*[lookup(q >> i, l) == int(math.log2(i)) if i != 0 else lookup(q >> i, l) == 0 for i in range(256)], q >> 128 == 0, l & 0xffffffff == 0)

ffs uses magic numbers found via z3.

from z3 import *

lookup = lambda x, q, l: (l >> ((31 - ((q / x if x > 0 else 0) & 31)) << 3)) & 0xff

l = BitVec('l', 256)
q = BitVec('q', 256)

solve(*[lookup(1 << i, q, l) == i for i in range(32)], lookup(0, q, l) == 0)