perf: faster Nat.testBit

[FR-vdash-bot]

1 &&& n is faster than n &&& 1 for big n.

---

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f74980ccee82ca2abdae65dcbc5571d4640ed076 --onto 3035d2f8f689b52963f49b2414414913ca296953. (2024-05-16 06:50:42)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f74980ccee82ca2abdae65dcbc5571d4640ed076 --onto 3de60bb1f63efe9bb56380f911f86980b9f3332c. (2024-05-21 14:29:09)

[FR-vdash-bot]

awaiting-review

[alexkeizer]

Do you have numbers to confirm this claim?
Is it faster in kernel reduction or for compiled code? If it really is faster, doesn't the compiler just optimize it?

[FR-vdash-bot]

def test (x : Nat) : Nat := 1 &&& x
def test' (x : Nat) : Nat := x &&& 1

def run_test (n : Nat) (x : Nat) : IO Unit := do
  let mut t := 0
  for _ in [0 : n] do
    t := test x

def run_test' (n : Nat) (x : Nat) : IO Unit := do
  let mut t := 0
  for _ in [0 : n] do
    t := test' x

def n := 10^5
def x := 11^1000000

#eval timeit "1 &&& x" (run_test n x) -- 41ms
#eval timeit "x &&& 1" (run_test' n x) -- 1.5s

[alexkeizer]

That's a surprisingly big difference, almost suspiciously so. I only know enough about micro-benchmarking to know results can sometimes be misleading, so I tried playing with various variations (e.g., sprinkling no_inline) but everything points towards 1 &&& x indeed being significantly faster.

Admittedly, In my original comment I was only thinking about "small" (up-to 64 bit) numbers, is this x &&& 1 vs 1 &&& x a known behaviour of gmp (which I assume what is going on here, with the big numbers given in your testcase)?

[alexkeizer]

I'm not knowledgable enough about micro-benchmarks to say whether the given example doesn't have any weird inlining or other behaviour that might interfere with the numbers, but the difference does seem so significant that it makes sense to switch over.

Maybe we could have a much faster C implementation in the future.

For 64 bit or lower, bitwise and and shifting already have special cased code generation. I guess for larger numbers you could optimize indexing much more by using knowledge of the gmp representation, but we'd need some good evidence that the extra maintenance burden is worth the benefit. In any case, that's not a discussion relevant to this PR, so maybe just take that comment out of the PR description.

Otherwise, I've got a minor comment about the proof style but the rest LGTM