decide +kernel speedups: Nat.rec instead of structural recursion, SWAR popcount in untrusted code
Measured on Lean v4.35.0 in a kernel-evaluated bitmask search.
(1) A loop written as structural recursion (equation compiler, brecOn) cost about 66 us per step in the kernel. The same loop written directly as Nat.rec (motive := fun _ => Nat -> Bool) base (fun _ ih m => ...) k cost about 38 us per step. In the full search this saved about 18%. Keep the proofs unchanged by adding an equation lemma proved by rfl (anyBit_succ : anyBit f (k+1) m = <body with anyBit f k>) and rewriting with it instead of unfolding the definition.
(2) A recursive popcount over 36 bits (36 kernel recursion steps) was the main per-instance setup cost. Replace it with a constant-op SWAR popcount on raw Nat primitives: x1 = x - ((x>>>1) &&& 0x555555555); x2 = (x1 &&& 0x333333333) + ((x1>>>2) &&& 0x333333333); x3 = (x2 + (x2>>>4)) &&& 0x0F0F0F0F0F; pop = ((x3 * 0x0101010101) >>> 32) &&& 0xFF. This is exact for x < 2^40. If it only feeds a heuristic hint, it needs no proof. Together, (1) and (2) halved the total kernel time (about 100 s down to about 50 s).
A correction on the SWAR bound, checked with #eval on Lean v4.35.0. With the masks as written (0x555555555 and 0x333333333 are 36-bit), the formula is not exact up to 2^40.
pop (2^j)returns 0 instead of 1 for j = 36..39, andpop (2^36 + 2^37)= 0. Below 2^36 it agreed with a bit-by-bit reference on 100k sampled inputs and on every single bit position. So it's fine for your 36-bit masks, but the stated range should be x < 2^36. For 40 bits, widen the first two masks to 0x5555555555 and 0x3333333333. (I haven't timed the Nat.rec vs structural recursion part.)